import {Formula} from './formula.js'
import {isSubtypeOf} from './type.js'
import * as Term from './term.js'

Error.stackTraceLimit = 100

const unifiable = (formula1: Formula, formula2: Formula) => formula1.unify(formula2, new Map, new Map)
const termsUnifiable = (term1: Term.Term, term2: Term.Term) => term1.unify(term2, new Map, new Map)

const containsFormula = (formulae: Formula[], formula: Formula) =>
    formulae.some(formula_ => unifiable(formula_, formula))

export const eliminateFalse = (premises: Formula[]) => premises.includes(Formula.False)

const eliminateOrHelper = (formula: Formula, premises: Formula[], consequence: Formula): boolean =>
    formula instanceof Formula.Disjunction &&
    formula.operands.every(
        operand => premises.some(
            premise => premise instanceof Formula.Implication &&
            unifiable(premise.operands[0], operand) &&
            unifiable(premise.operands[1], consequence),
        ) ||
        eliminateOrHelper(operand, premises, consequence),
    )

export const eliminateOr = (premises: Formula[], consequence: Formula) =>
    premises.some(premise => eliminateOrHelper(premise, premises, consequence))

const eliminateImpliesHelper = (formula: Formula, premises: Formula[], consequence: Formula): boolean =>
    formula instanceof Formula.Implication &&
    containsFormula(premises, formula.operands[0]) &&
    (
        unifiable(formula.operands[1], consequence) ||
        eliminateImpliesHelper(formula.operands[1], premises, consequence) ||
        eliminateImplies(premises, formula.operands[1])
    )

export const eliminateImplies = (premises: Formula[], consequence: Formula) =>
    premises.some(premise => eliminateImpliesHelper(premise, premises, consequence))

const eliminateAndHelper = (premise: Formula, consequence: Formula): boolean =>
    premise instanceof Formula.Conjunction &&
    premise.operands.some(
        operand => unifiable(operand, consequence) || eliminateAndHelper(operand, consequence),
    )

export const eliminateAnd = (premises: Formula[], consequence: Formula) =>
    premises.some(premise => eliminateAndHelper(premise, consequence))

export const eliminateFor = (premises: Formula[], consequence: Formula): boolean =>
    premises.some(premise => {
        if (!(premise instanceof Formula.Generalization))
            return false

        const subquantor = premise.operand.substitute(
            new Map([[premise.variable, new Term.MetaVariableTerm(premise.variable)]]),
        )

        return unifiable(subquantor, consequence) ||
            eliminateFor([subquantor], consequence)
    })

export const insertOr = (premises: Formula[], consequence: Formula): boolean =>
    consequence instanceof Formula.Disjunction &&
    consequence.operands.some(
        operand =>
            containsFormula(premises, operand) ||
            insertOr(premises, operand),
    )

export const insertTrue = (premises: Formula[], consequence: Formula) => consequence === Formula.True

export const insertAnd = (premises: Formula[], consequence: Formula): boolean =>
    consequence instanceof Formula.Conjunction &&
    consequence.operands.every(
        operand =>
            containsFormula(premises, operand) ||
            insertAnd(premises, operand),
    )

export const insertEx = (premises: Formula[], consequence: Formula): boolean => {
    if (!(consequence instanceof Formula.Existence))
        return false

    const subquantor = consequence.operand.substitute(
        new Map([[consequence.variable, new Term.MetaVariableTerm(consequence.variable)]]),
    )

    return containsFormula(premises, subquantor) ||
        insertEx(premises, subquantor)
}

export const insertIs = (_: Formula[], consequence: Formula) =>
    consequence instanceof Formula.TypeAssertion &&
    isSubtypeOf(consequence.parameter.getType(), consequence.type)

export const insertEquality = (_: Formula[], consequence: Formula) =>
    consequence instanceof Formula.Equality &&
    termsUnifiable(consequence.left, consequence.right)

export const reiterate = (premises: Formula[], consequence: Formula) =>
    containsFormula(premises, consequence)
